Papers with formal reasoning tasks
Rosetta-PL: Propositional Logic as a Benchmark for Large Language Model Reasoning (2025.naacl-srw)
Copied to clipboard
Shaun Lee Baek, Shaun Esua-Mensah, Cyrus Tsui, Sejan Vigneswaralingam, Abdullah Alali, Michael Lu, Vasu Sharma, Kevin Zhu
| Challenge: | Large Language Models (LLMs) are primarily trained on high-resource natural languages, limiting their effectiveness in low-resourced settings and in tasks requiring deep logical reasoning. |
| Approach: | They propose to use a dataset of logical propositions from Lean into a custom logical language to evaluate LLMs' logical reasoning and generalization capabilities in a controlled environment. |
| Outcome: | The proposed model improves accuracy and accuracy beyond 20,000 training samples. |
Efficient PRM Training Data Synthesis via Formal Verification (2026.findings-acl)
Copied to clipboard
Ryo Kamoi, Yusen Zhang, Nan Zhang, Sarkar Snigdha Sarathi Das, Ranran Haoran Zhang, Wenpeng Yin, Rui Zhang
| Challenge: | Existing approaches for constructing PRM training data rely on human annotation or sampling-based labeling methods that require repeated LLM calls. |
| Approach: | They propose a framework that synthesizes PRM training data by annotating step-level error labels using formal verification tools such as Z3 and Isabelle. |
| Outcome: | The proposed framework synthesizes PRM training data from formal logic and theorem proving tasks without human annotation or additional LLM calls. |
Unravelling the Logic: Investigating the Generalisation of Transformers in Numerical Satisfiability Problems (2025.acl-long)
Copied to clipboard
| Challenge: | Transformer models exhibit minimal scale and noise invariance, along with limited vocabulary and number invariancy. |
| Approach: | They probe the generalisation prowess of Transformer models with respect to the hitherto unexplored domain of numerical satisfiability problems. |
| Outcome: | The proposed models exhibit minimal scale and noise invariance, along with limited vocabulary and number invariancy. |